x,y:Atom. (x =a y)  (x = y) 

latex

ProofTree

Definitions	, t  T, P  Q, P  Q, P  Q, x =a y, P  Q, x:A. B(x), True, T, if b then t else f fi , tt, b, P  Q, Dec(P), False, A, ff
Lemmas	bfalse wf, btrue wf, assert wf, decidable atom equal, bool wf, true wf, squash wf